$\forall$${\it es}$:event\_system\{i:l\}, $e$:es{-}E(${\it es}$), $t$:rationals.
\\[0ex]es{-}state{-}after{-}elapsed(${\it es}$; $e$; $t$) $\in$ es{-}state(${\it es}$; loc($e$))